#include <windows.h>
#include <oleauto.h>
#include <string>

#include "node.h"
#include "generalizer.h"
#include "input.h"
#include "prover.h"
#include "system.h"

extern "C"__stdcall __declspec(dllexport) Rules *createSystem () {
  return new Rules;
}

extern "C"__stdcall __declspec(dllexport) void deleteSystem (Rules *rules) {
  delete rules;
}

extern "C"__stdcall __declspec(dllexport) void assertz (
    Rules *rules, const char *s) {
  pNode node (s);
  rules->assertz (node);
}

extern "C"__stdcall __declspec(dllexport) int query (
    Rules *rules, const char *s) {
  bool result;
  Trail trail;
  System system (*rules, trail);
  pNode node (s);
  pNode generalizedNode = generalize (*node);
  Prover *prover = Prover::create (*generalizedNode, system);
  result = prover->prove ();
  delete prover;

  if(result)
  return -1; // vbTrue
  else
  return 0; // vbFalse
}

extern std::vector<std::string> outputStrings;

extern "C"__stdcall __declspec(dllexport) int nOutputs () {
  return outputStrings.size ();
}

extern "C"__stdcall __declspec(dllexport) BSTR output (int n) {
  const char *source = outputStrings[n].c_str ();

  /* Okay this works, don't think too much */
  return SysAllocString ((const OLECHAR*) source);
}

// Passes value back to the dll
std::vector<std::string> outputStrings;

class output : public OnceProver {
predicateName("output")

  bool proveOnce () {
    outputStrings.clear ();
    for(std::vector<pNode>::iterator p = tuple->nodes.begin () + 1; p
        < tuple->nodes.end (); p++)
      outputStrings.push_back (p->display ());
    return true;
  }

  Tuple *tuple;
  void set (Tuple &t, System&) {
    tuple = &t;
  }
};

ProverFactoryRegistrar<output, Tuple::ID> outputRegistrar;
